ESMachineAxiom(E;T;V;M;loc;knd;val;
when;after;
sndr;Trans;Send;Choose)
== (e:E. (x.after(x,e)) = Trans(loc(e),knd(e),val(e),x.when(x,e)))
== & (e:E.
== & ((islocal(knd(e)))
== & ( ((isl(Choose(loc(e),act(knd(e)),x.when(x,e))))
== & ( c (val(e) = outl(Choose(loc(e),act(knd(e)),x.when(x,e))))))
== & (e:E.
== & ((isrcv(knd(e)))
== & ( (<lnk(knd(e)), tag(knd(e)), val(e)>  Send
== & ( (<lnk(knd(e)), tag(knd(e)), val(e)>  (loc(sndr(e))
== & ( (<lnk(knd(e)), tag(knd(e)), val(e)>  ,knd(sndr(e))
== & ( (<lnk(knd(e)), tag(knd(e)), val(e)>  ,val(sndr(e))
== & ( (<lnk(knd(e)), tag(knd(e)), val(e)>  ,x.when(x,sndr(e))))) 

latex

---

clarification:

ESMachineAxiom(E;T;V;M;loc;knd;val;
when;after;
sndr;Trans;Send;Choose)
== (e:E. (x.after(x,e)) = Trans(loc(e),knd(e),val(e),x.when(x,e))  x:IdT(loc(e),x))
== & (e:E.
== & ((islocal(knd(e)))
== & ( ((isl(Choose(loc(e),act(knd(e)),x.when(x,e))))
== & ( c (val(e) = outl(Choose(loc(e),act(knd(e)),x.when(x,e)))  V(loc(e),act(knd(e))))))
== & (e:E.
== & ((isrcv(knd(e)))
== & ( (<lnk(knd(e)), tag(knd(e)), val(e)>  Send
== & ( (<lnk(knd(e)), tag(knd(e)), val(e)>  (loc(sndr(e))
== & ( (<lnk(knd(e)), tag(knd(e)), val(e)>  ,knd(sndr(e))
== & ( (<lnk(knd(e)), tag(knd(e)), val(e)>  ,val(sndr(e))
== & ( (<lnk(knd(e)), tag(knd(e)), val(e)>  ,x.when(x,sndr(e)))  Msg(M))) 

latex

Definitions	x:AB(x), Id, P & Q, islocal(k), A c B, isl(x), s = t, outl(x), act(k), x:A. B(x), P  Q, b, isrcv(k), (x  l), lnk(k), <a, b>, tag(k), x.A(x), f(a), Msg(M)
FDL editor aliases	ESMachineAxiom